proofs: expose native EVMYulLean transition target#1743
proofs: expose native EVMYulLean transition target#1743
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fc6b2b9c8a
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
Th0rgal
force-pushed
the
codex/native-evmyullean-transition
branch
from
0672929 to
39ae307
Compare
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 39ae307375
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 4f58dad. Configure here.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b28b535b6a
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c62fc97e30
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| def materializedStorageSlots | ||
| (runtimeCode : List YulStmt) | ||
| (observableSlots : List Nat) : | ||
| List Nat := | ||
| yulStmtsLiteralStorageReadSlots runtimeCode ++ observableSlots |
There was a problem hiding this comment.
materializedStorageSlots only preloads literal sload slots plus caller-supplied observableSlots, but the emitted runtime frequently reads storage through computed slots (for example mapping/dynamic-array paths lowered to sload(mappingSlot(...))). Those computed read slots are absent from initialState, so native execution sees them as zero and can take different branches or write different results than source semantics unless the caller manually precomputes every read slot. This makes interpretRuntimeNative behavior input-dependent on an incomplete preload set and can silently corrupt native/source equivalence for contracts that branch on mapping values.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b462beb0c2
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| Used by `modifies(...)` validation (#1729, Axis 3 Step 1b). -/ | ||
| def stmtWrittenFields : Stmt → List String | ||
| | Stmt.setStorage field _ | Stmt.setStorageAddr field _ | ||
| | Stmt.setStorage field _ | Stmt.setStorageAddr field _ | Stmt.setStorageWord field _ _ |
There was a problem hiding this comment.
stmtWrittenFields treats Stmt.setStorageWord as a write to just the root field name, but lowering executes sstore(field.slot + wordOffset, ...) (and alias mirrors), so nonzero offsets can mutate different declared fields. A function annotated modifies(root) can therefore pass validation while writing outside the declared set (for example, setPackedStorage root 1 ... clobbering the next slot), which makes the generated modifies/frame guarantees unsound. The modifies check should either reject nonzero wordOffset here or compute touched fields from resolved slots instead of the root field label.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 81b7d3478b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| match fn.params.toList.map (fun p => valueTypeSignatureComponent p.ty) with | ||
| | [] => "0" | ||
| | parts => String.intercalate "_" parts |
There was a problem hiding this comment.
overloadedFunctionIdentName builds suffixes by joining per-parameter type components with _, but those components already contain underscores, so the mapping is not injective. A legal overload set can therefore collapse to the same generated identifier (e.g., one-arg newtype_n_scalar_uint256 over Uint8 vs. two args newtype_n over Uint256 and Uint8 both produce newtype_n_scalar_uint256_scalar_uint8), and validateGeneratedDefNamesPublic then rejects it as a duplicate internal declaration. This turns valid overloads into deterministic compile failures; the suffix encoding needs explicit boundaries (such as length-prefixing each component).
Useful? React with 👍 / 👎.
2 participants
Summary
Native.interpretIRRuntimeNativeas the executable native EVMYulLean target for emitted IR runtime YulYulResultEvmYul.Yul.callDispatcherFixed issues
Closes #1738.
Closes #1739.
Closes #1740.
Closes #1741.
Closes #1742.
Closes #1744.
Closes #1745.
Refs #1737.
Refs #1722.
Why
PR #1735 was only a docs/sync cleanup and did not close the native-runtime work from #1722. The current public theorem target still runs through
interpretYulRuntimeWithBackend .evmYulLean, which uses Verity's custom Yul statement interpreter with EVMYulLean-backed builtins. That bridge is useful, but it is not the simpler final architecture requested in #1737.This PR is now the native transition foundation plus the reported frontend/executable parity fixes needed before the remaining work can focus on the native public theorem target.
What changed
Native.interpretIRRuntimeNativeoverEvmYul.Yul.callDispatcher.verity_contractenvironment reads such asblockTimestamp,blockNumber,chainid,blobbasefee,contractAddress,msgSender, andmsgValue, including executable.runstate reads.internalCall/internalCallAssignremain only lower-level compilation-model IR.setPackedStorage root offset word, lowering toStmt.setStorageWord/sstore(root.slot + offset, word).arrayLength/arrayElement; dynamic element arrays such asArray StringandArray Bytesstill fail closed.Remaining work for #1737
Native.interpretIRRuntimeNativeor a total wrapper around itexecYulFuel/execYulFuelWithBackendto reference-oracle status and update trust-boundary docs accordinglyValidation
lake build Contracts.Smokelake build Contracts.MacroTranslateInvariantTestlake build Contracts.MacroTranslateRoundTripFuzzlake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeSmokeTestpython3 scripts/check_selectors.pypython3 -m unittest scripts/test_native_transition_api.py scripts/test_check_native_transition_doc.py scripts/test_check_selectors.py -vpython3 -m unittest scripts/test_generate_macro_property_tests.py -vpython3 scripts/check_macro_property_test_generation.pypython3 scripts/check_lean_hygiene.pypython3 scripts/check_verification_status_doc.pypython3 scripts/check_layer2_boundary_sync.pypython3 scripts/check_layer2_boundary_catalog_sync.pypython3 scripts/check_docs_workflow_sync.pygit diff --checkmake checkNote
Medium Risk
Adds new compiler IR constructs and modifies dispatch/ABI helper generation plus large proof-surface changes around a new native EVMYulLean execution seam; mistakes could change emitted Yul/storage semantics or invalidate conformance guarantees.
Overview
Exposes a native EVMYulLean execution target for emitted runtime Yul by extending
Compiler/Proofs/EndToEnd.leanwith new comparison surfaces (nativeResultsMatchOn,yulResultsAgreeOn) and explicit bridge obligations that relateNative.interpretIRRuntimeNative/callDispatcherresults to the existing EVMYulLean-backed interpreter oracle.Extends the compilation model and codegen to support (1) word-level access into dynamic-array elements via
Expr.arrayElementWordplus new checked helper functions, and (2) full-word storage writes atfield.slot + offsetviaStmt.setStorageWord(including mirroring alias slots). It also refines ABI/dynamic-array bounds checks to account for multi-word static elements.Tightens validation/dispatch rules by treating external overloads as unique by function signature (not just name), adds explicit checks for duplicate/colliding internal function names, and updates reserved-symbol collision detection to include the new helper names. Updates CI/docs conformance guard messaging to include the native harness/oracle coverage and adds targeted smoke tests/regressions for the new features and name-collision diagnostics.
Reviewed by Cursor Bugbot for commit 019a943. Bugbot is set up for automated code reviews on this repo. Configure here.